We carry out a systematic study of decidability for theories of real vector spaces, inner product spaces, and Hilbert spaces and of normed spaces, Banach spaces and metric spaces, all formalized using a 2-sorted first-order language. The theories for list turn out to be decidable while the theories for list are not even arithmetical: the theory of 2-dimensional Banach spaces, for example, has the same many-one degree as the set of truths of second-order arithmetic.We find that the purely universal and (...) purely existential fragments of the theory of normed spaces are decidable, as is the ∀∃ fragment of the theory of metric spaces. These results are sharp of their type: reductions of Hilbertʼs 10th problem show that the ∃∀ fragments for metric and normed spaces and the ∀∃ fragment for normed spaces are all undecidable. (shrink)

We show that strong measure zero sets -totally bounded metric space) can be characterized by the nonexistence of a winning strategy in a certain infinite game. We use this characterization to give a proof of the well known fact, originally conjectured by K. Prikry, that every dense \ subset of the real line contains a translate of every strong measure zero set. We also derive a related result which answers a question of J. Fickett.

Hofstadter has introduced the notion of an explicit Henkin sentence. Roughly speaking, an explicit Henkin sentence not only asserts its own provability, as ordinary Henkin sentences do, but explicitly provides a detailed description of a proof. We provide, in this paper, a precise formalization of Hofstadter's notion and then show that true explicit Henkin sentences exist.